A:Type, B:(AType), f:a:A fp B(a), eq:EqDecider(A), x:A, z:B(x). f(x)?z  B(x) 

latex

Definitions	f(x)?z, Unit, P  Q, P & Q, x  dom(f), f(x), , Prop, b, A, b, x. t(x), P  Q, strong-subtype(A;B), x:A. B(x), EqDecider(T), a:A fp B(a), x(s), Top, t  T
Lemmas	strong-subtype-self, top wf, subtype-fpf3, assert wf, not wf, bnot wf, fpf-ap wf, bool wf, fpf-dom wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, fpf wf, deq wf